package ch.epfl.lara.pm.analyze;

import ch.epfl.lara.pm.ast._
import ch.epfl.lara.pm.util.MyImplicitConversions
import ch.epfl.lara.pm.parser.PrettyPrinter
import ch.epfl.lara.pm.global.{ClassTable,ObjectTable}

import ch.epfl.lara.pm.analyze.set._



class Verify(constraints: Formula, guardsConstraint: List[Expr], matchExpr: Match, map: PatternMap) extends FormulaBuilder with MyImplicitConversions{
  import ch.epfl.lara.pm.formdecider.{FormDeciderWrapper,FormDeciderFormulaStringer}
  
  val cases: List[CaseDef] = matchExpr.cases
  var patsAsSets: List[List[String]] = _
  
  var nestedToVerify: List[Verify] = Nil
  var axioms: Formula = constraints
  
  var isNested = false
 
  def this(isNested: Boolean, constraints: Formula, guardsConstraint: List[Expr], matchExpr: Match, map: PatternMap) {
    this(constraints: Formula, guardsConstraint: List[Expr], matchExpr: Match, map: PatternMap)
    this.isNested = isNested

    initialize
  }
  
  
  def initialize {
    transform
    nestedPatterns
  }
  
  
  private def transform {
    val Match(_,tpe,kases) = matchExpr
    val ipatterns = kases.map(kase => PatternConverter(kase.pattern))
    val refinedPats =  RefineIPatterns(map,ipatterns,tpe)
    patsAsSets = IPatternsAsSets(map,refinedPats)
    
    axioms = And(axioms,conjunctionMultiSet(map.getCompleteSet))
  }
  
  
  private def nestedPatterns {
    val nestedMatch = for(kase<-cases) yield (Util.findMatchExpressions(kase.body),kase.position)
    
    nestedToVerify = (for((list,pos)<-nestedMatch;nested<-list) yield {
      val nmap = if(isNested) map.clone() else new PatternMap
      val pat = cases(pos).pattern
      
      RefineIPatterns(nmap,List(PatternConverter(pat)),pat.getTpe)
      
      new Verify(true,constraints,guardsConstraint ::: List(cases(pos).guard.getOrElse(True)),nested,nmap)
    })
  }
  
  
  
  
  def verifyCompleteness: Option[Warning] = { 
    verifyCompletenessCurrentMatch match {
      case (true,_) =>  verifyCompletenessNestedMatches
        
      case (false,incomplete) => Some(CompletenessFailed(incomplete.map(cases(_).pattern.getTpe)))
    }
  
  }
  
  
  
  
  private def verifyCompletenessCurrentMatch: (Boolean,List[Int]) = {
    val (complete,incomplete) = splitCompleteAndIncompletePatterns(patsAsSets.length)
    
   //val completeset = conjunctionSet(map.getCompleteSet)
    val patternsset = complete.map(patsAsSets(_))
    val completeness = Imply(axioms,dnfSets(patternsset)) //Imply(constraints,Imply(completeset,dnfSets(patternsset)))
                                                          //println(FormDeciderFormulaStringer(completeness)+"\n")
    (checkFormula(completeness),incomplete)
  }
  
  
  
  
  private def verifyCompletenessNestedMatches: Option[Warning] = { 
    var errors: List[(Match,Warning)] = Nil
    for(nested<-nestedToVerify)  {
      val verified = nested.verifyCompleteness
      if(verified.isDefined) {
        errors = (nested.getMatch,verified.get) :: errors
      }
    }
    
    if(errors.isEmpty) None
    else Some(NestedMatchesFailed(errors))
  }
  
  

  private def splitCompleteAndIncompletePatterns(bound: Int): (List[Int],List[Int]) = {
    val complete_patterns = patternsWithoutGuards(bound)
    val (complete,incomplete) = collectCompletePatterns(List.range(0,bound).diff(complete_patterns))
    (complete_patterns.union(complete),incomplete)
  }
  
  
  
  private def patternsWithoutGuards(bound: Int): List[Int] =
    for(CaseDef(pos,_,guard,_)<-cases if pos < bound && guard.isEmpty) yield pos
 
    
    
    
  private def collectCompletePatterns(patternIndex: List[Int]) = {
    var complete: List[Int] = Nil
    var incomplete: List[Int] = Nil
    
    for(listIndex<-wrapTogetherIdenticalSets(patternIndex)) {
      val conditions = listIndex.map(cases(_).guard.getOrElse(True))
      val formula = guardsConstraint.foldRight[Expr](dnfExprs(conditions))((x,acc) => EImply(x,acc))
                                                   //println("Testing formula for guards: "+FormDeciderFormulaStringer(formula))
      if(checkFormula(formula)) 
        complete = listIndex.head :: complete
      
      else 
        incomplete = listIndex.head :: incomplete
    }
    (complete,incomplete.removeDuplicates)
  }
  
  
  
  
  
  def wrapTogetherIdenticalSets(indexes: List[Int]): List[List[Int]] = indexes match {
    case Nil => Nil
    case head :: tail => 
      val identical = for(i<-tail if patsAsSets(head) == patsAsSets(i)) yield i
      (head :: identical) :: wrapTogetherIdenticalSets(tail.diff(identical))
  }
  
  

   
  def verifyDisjointness: Option[Warning] = {
    (collectOverlappingCases ::: nestedToVerify.flatMap(_.collectOverlappingCases)) match {
      case Nil => None
      case overlapping => Some(DisjointnessFailed(overlapping))
    }
  }
  
  
  private def collectOverlappingCases: List[(CaseDef,CaseDef)] = {
    val length = patsAsSets.length
    
    for(i<-List.range(0,length);j<-List.range(i+1,length);
      if(areOverlapping(i,j))) yield  (cases(i),cases(j))
  }
  
  
  
  
  private def areOverlapping(i: Int, j: Int): Boolean = 
    arePatternsOverlapping(i,j) && areGuardsOverlapping(i,j)
  
    
    
    
  private def arePatternsOverlapping(i: Int, j: Int): Boolean = {
    val formula = disjointUnionSet(patsAsSets(i),patsAsSets(j))
    !checkFormula(Imply(constraints,formula))
  }
  
  
  
  
  private def areGuardsOverlapping(i: Int, j: Int): Boolean = {
    val res = (cases(i).guard,cases(j).guard) match {
      case (None,None) => false
      case (None,Some(cond)) => checkFormula(disjointUnionExpr(cond,True))
      case (Some(cond),None) => checkFormula(disjointUnionExpr(cond,True))
      case (Some(cond1),Some(cond2)) => checkFormula(disjointUnionExpr(cond1,cond2))
    }
    !res
  }
  
  
  
  def verifyReachability: Option[Warning] = {
    verifyExtractorsReachability.orElse(verifyReachabilityCurrentMatch) match {
      case None =>  verifyReachabilityNestedMatches
        
      case Some(kase) => Some(kase)
    }
  
  }
  
  
  private def verifyExtractorsReachability: Option[Warning] = {
    val set = map.getCompleteSet
    for(i<-List.range(0,patsAsSets.length)) {
      val patset = patsAsSets(i)
      assert(set.size == patset.size)
      
      for(j<-List.range(0,patset.size)) {
        val head = set(j).head
        if(head == ClassTable.root || patset(j) == ClassTable.root) ()
        else {
        val thisC = (if(ClassTable.containsClass(head)) {
          ClassTable.lookupClass(head)
        } else {
          ClassTable.lookupClass(ObjectTable.getExtractorType(head))
        })
        
        val thatC = (if(ClassTable.containsClass(patset(j))) {
          ClassTable.lookupClass(patset(j))
        } else {
          ClassTable.lookupClass(ObjectTable.getExtractorType(patset(j)))
        })
        
        if(thisC.lub(thatC).isEmpty)
          return Some(ReachabilityExtractorsFailed(cases(i)))
        }
      }
    }
    None
  }
  
  
  private def verifyReachabilityCurrentMatch: Option[Warning] = { 
    for(i<-List.range(0,patsAsSets.length-1)) {
      val (complete,incomplete) = splitCompleteAndIncompletePatterns(i+1)
      
      complete match {
        case Nil => ()
        case sets =>
          val subsume = Imply(Imply(axioms,conjunctionSet(patsAsSets(i+1))),dnfSets(complete.map(patsAsSets(_))))
          if(checkFormula(subsume)) {
          //  println(FormDeciderFormulaStringer(subsume)+"\n")
            return Some(ReachabilityFailed(cases(i+1)))
          }
      }
      
      val identical = (for(j<-List.range(0,i+1) ) yield {
        if(patsAsSets(j) == patsAsSets(i+1))
          List(cases(j).guard.getOrElse(True))
        else {
          Nil
        }
      }).flatMap(p=>p)
      
      val subsume = EImply(conjunctionExprs(cases(i+1).guard.getOrElse(True) :: guardsConstraint),dnfExprs(identical))
      
      if(checkFormula(subsume)) 
        return Some(ReachabilityFailed(cases(i+1)))
      
    }
    
    None 
  }
  
  
  private def verifyReachabilityNestedMatches: Option[Warning] = {
    for(nested<-nestedToVerify)  {
      val verified = nested.verifyReachability
      if(verified.isDefined) {
        return Some(NestedMatchesFailed(List((nested.getMatch,verified.get))))
      }
    }
    
    None
  }
  
  
  
  private def checkFormula(formula: Formula): Boolean = FormDeciderWrapper.decide(FormDeciderFormulaStringer(formula))
 
  private def checkFormula(formula: Expr): Boolean = FormDeciderWrapper.decide(FormDeciderFormulaStringer(formula))
 
  
  def getMatch = matchExpr
  
  override def toString = "Verify"
}
